Welcome to the last session of the semester.

I have a little bit more to do. You have to ask something in the exam.

We still have the PSPACE hardness test open for the K performance.

The idea was to reduce TQBF.

We had a formula in TQBF, a quantified Buhl's formula, a closed one, only for such TQBF defined.

It is in TQBF, in other words, it evaluates to truth.

Exactly, when a TQBF has a quantified Buhl's formula, a witness for truth, as well as the statement of a fulfilling TQBF,

it is a pure propositional formula.

I repeat the example we had.

This formula here, for all x, exists a y, so that x is equivalent to non-y.

I will now draw the quantum tree, without repeating the formal definition, which you could hopefully guess from the picture.

So the quantum tree has...

Let's see if that's enough.

So the quantum tree has...

If there are n quantas, n plus 1 levels, here there are two quantas, so it has calculated the roots on three levels.

On each level, the evaluation of another variable is determined, i.e. the quantified variable.

Here in the root, no variable is determined.

The distribution of the tree always corresponds to the quantas.

So if I have an existing quantum, I always have to give one value, i.e. a witness, for the existing quantum, whether true or false.

If I see an all-quantum, I have to try out all possible Buhl's values.

Well, that's only two, so I have a degree of devaluation 2 at this point, where I try out both possible values on both sides,

but show that it works in both cases.

So here I have, for this formula, in levels, how did I want to number the levels?

I wanted to number the levels, here at the beginning with zero.

This is quantum 1, this is quantum 2, so here are levels 1 and 2 for these two quantas.

So here I have, let's say, how did I want to do it? Left, false, right, true.

These are the two values ​​I try out for x.

So here I have my quantum for all x, for which I am looking for a witness.

That means I need a witness for false and one for x equal true.

And then I have an existing quantum, exists y, so I have to indicate only one every time, which is why it works.

So I always have only one successor. Well, here I give it to true and here I give it to false.

And I always have to check that in the end, actually my formula under the quantas,

which is fulfilled by the evaluation that I collect by running from the root to this plate.

So here I have what? x equal true and y equal false. Well, that's obvious.

And here I have x equal true and y equal false and that's obvious too.

So that means a witness for the truth of a closed QBF formula is such a quantum structure.

So now comes the idea for our reduction from TQBF to completeness in modal logic.

Let's go over the basic principle. So I have given such a closed quantified Boulge formula in prenexanormal form,

which is the same as in Gleun.

So, to such a thing we are now constructing a modal formula.

And it is clear that the reduction function has to look like this.

The reduction of one problem to another takes an instance of the problem to be reduced.

So we have a modal formula, which we call F phi. And we build it in such a way that

phi has a quantum tree, which I will briefly abbreviate as QB.

And that is when F of phi is achievable. And we will do this by extracting a quantum tree from a model of F phi.

So, this is the global one. And now comes the nitty-gritty.

So now we write this formula here. And after seeing the formula, the exponential size of the model is forced,

which is quite similar to this one. You would guess that this would fit a graph.

So, F phi is now a list of axioms. Of course, F of phi is the conjunction of these things. And I will numerate these axioms.

The idea is the same as in the exercise.